st-lookup(tab;x)
== let K,p,f = tab in 
== let n = mu(n.p <z n K z n (f(n)).1 =a1 x) in
== let nif p <z n K z n then inr   else inl ((f(n)).2)  fi  

latex

---

clarification:

st-lookup(tab;x)
== let K,p,f = tab in 
== let n = mu(n.p <z n K z n eq_atom1((f(n)).1;x)) in
== let nif p <z n K z n then inr   else inl ((f(n)).2)  fi  

latex

Definitions	let x,y,z = a in t(x;y;z), let x = a in b(x), mu(f), x.A(x), eq_atom$n(x;y), t.1, if b then t else f fi , p q, i <z j, i z j, inr x , , inl x , t.2, f(a)
FDL editor aliases	st-lookup